A:Type, eq:EqDecider(A), B:Top, x, y:A, v, u:Top. ((x = y))  x : v || y : u 

latex

Definitions	False, P  Q, A, t  T, Top, x.A(x), x:A. B(x), x. t(x), x : v, x  dom(f), b, x:A  B(x), , P & Q, x:AB(x), f(a), x(s), s = t, f || g, Type, EqDecider(T), left + right, P  Q, Void, <a, b>, eqof(d), P  Q, P  Q, ff, p q
Lemmas	assert of bor, bor wf, bfalse wf, and functionality wrt iff, or functionality wrt iff, deq property, eqof wf, false wf, not wf, deq wf, assert wf, fpf-dom wf, fpf-single wf, top wf